﻿/*****************************************************
 * File:            
 * Description:    
 * By:              Ali Khalili (khalili DOT ir AT gmail DOT com)
 * Project:         Name of Project
 * Requirements:    
 * Change log:                - 10 Jan 2014: Bug fix (distinguishing state was not working)
 * 
 *          
 * To Do:           -
 * NOTE:                        - AS not all distinguishing things are enabled,
 *                                           we should choose enabled onses!
 * License:
************************************************************
 * W-Method
 * Assumptions:
 * 1. M is Completely specified, minimal, connected, and deterministic.
 * 2. M starts in a fixed initial state.
 * 3. M and IUT (Implementation Under Test) have the same input alphabet.
 *
 *
 * Transition cover set for machine M, denoted as P, is a finite
 * set of input sequences such that exciting M with all
 * elements of P ensures that all states are reached and all
 * transitions are traversed at least once.
 * --- P is constructed from the testing tree of M.
 * Each test case t is of the form r.s where r is in P and s in W.
 * r moves the application from initial state q0 to state qj.
 * Then, s=as’ takes it from qi to state qj or qj’.
 *
 * Overal steps:
 * Step 1: Estimate m, the number of states in the correct implementation of the given FSM M.
 *         Let us assume that m is available from the design specification. *
 *         Or
 *         Since we do not have access to the correct implementation, we
 *         assume that m = n, the number of states in M (i.e., implementation         under test).
 * Step 2: Construct the characterization set W for M.
 *         Let M=(X, Y, Q, q1, δ, O) be a minimal and complete FSM.
 *         W is a finite set of input sequences that distinguish the behavior of
 *         any pair of states in M. Each input sequence in W is of finite length.
 *         Given states qi and qj in Q, W contains a string s such that:
 *         O(qi,s)≠O(qj,s)
 *        
 *         Step 1: Construct a sequence of k-equivalence partitions of Q denoted
 *                 as P1, P2, …Pm, m>0.
 *         Step 2: Traverse the k-equivalence partitions in reverse order to obtain
 *                 distinguishing sequence for each pair of states.
 *
 * Step 3: Construct the testing tree for M and generate the transition
 * cover set P from the testing tree.
 * Step 4: Construct set Z from W and m.
 * Step 5: Desired test set=P.Z
******************************************
 * Wp (partial) method:
 *         Tests are generated from minimal, complete, and connected FSM.
 *         Size of tests generated is generally smaller than that generated using the W-method.
 *         Test generation process is divided into two phases:
 *                 Phase 1: Generate a test set using the state cover set (S) and the characterization set (W).
 *                 Phase 2: Generate additional tests using a subset of the transition cover set and state identification sets.
*****************************************************/
using System;
using System.Collections.Generic;
using System.Collections;
using SMLib.Automata.Base;
using SMLib.Base;
using SMLib.Automata.DFA;
using SMLib.Automata.MM;
using MBT.Utils;

namespace MBT.Conformance.OfflineTesting
{
	/// <summary>
	/// W Method for test case generation/equivance query for Deterministic Systems
	/// <remarks>[based on "Testing Software Design Modeled by Finite State Models, 1987"]
	/// <para>
	/// Assumption:
	/// - M is Completely specified, minimal, connected, and deterministic.
	/// - M starts in a fixed initial state.
	/// - M and IUT (Implementation Under Test) have the same input alphabet.
	/// - The input alphabet is fixed and enumerable
	/// </para>
	/// <para>
	/// Steps:
	/// - Step 1: Estimate m, the number of states in the correct implementation of the given FSM M.
	/// - Step 2: Construct the characterization set W for M.
	/// - Step 3: Construct the testing tree for M and generate the transition cover set P from the testing tree.
	/// - Step 4: Construct set Z from W and m.
	/// - Step 5: Desired test set=P.Z
	/// </para>
	/// </remarks>
	/// </summary>
	public class OTCG_WMethod<STATETYPE, TRANSITIONTYPE>
	{
		protected IDiGraph<STATETYPE, TRANSITIONTYPE> testModel;
		protected List<Word> DistinguishingWords;
		protected List<Word> transitionCoverSet;
		//P ?
		protected List<Word> stateCoverSet;
		//P ?
		protected bool processed;
		protected bool computeStateCover;

		/// <summary>
		/// Constructor
		/// <remarks>When we use Mealy machine learning, we don't need to compute distinguishing set because we already have it</remarks>
		/// </summary>
		/// <param name="testModel">underlying test model</param>
		/// <param name="distinguishingWord">the set of state distinguishing words (optional)</param>
		public OTCG_WMethod (IDiGraph<STATETYPE, TRANSITIONTYPE> testModel, List<Word> distinguishingWord = null)
		{
			//* use this in Wp-Method
			computeStateCover = false;
			processed = false;
			this.testModel = testModel;
			this.DistinguishingWords = distinguishingWord;
		}
		#region internal computation of W-Method
		/// <summary>
		/// Generating transition cover set P by constructing the testing tree for M
		/// <remarks>
		/// <para>Transition cover set for machine M, denoted as P, is a finite
		/// set of input sequences such that existing M with all
		/// elements of P ensures that all states are reached and all
		/// transitions are traversed at least once.
		/// - P is constructed from the testing tree of M. </para>
		/// <para>A testing tree of an FSM is a tree rooted at the initial state. It contains at least
		/// one path from the initial state to the remaining states in the FSM. Here is
		/// how we construct the testing tree.
		/// -State q0, the initial state, is the rootof the testing tree. Suppose that the testing
		/// tree has been constructed until level k. The (k+1)th level is built as follows.
		/// -Select a node n at level k. If n appears at any level from 1 through k-1 , then n is
		/// a leaf node and is not expanded any further. If n is not a leaf node then we
		/// expand it by adding a branch from node n to a new node m if  δ(n, x)=m for
		/// each x in X . This branch is labeled as x. This step is repeated for all nodes at
		/// level k</para>
		/// </remarks>
		/// </summary>
		protected void FindTransitionCoverSet ()
		{
			//* this can be used also for transition coverage test case generation!
			Tree<STATETYPE, TRANSITIONTYPE> testTree = new Tree<STATETYPE, TRANSITIONTYPE> (testModel.GetStates () [0]);

			List<Tree<STATETYPE, TRANSITIONTYPE>.TreeNode> treeFrontiers = new List<Tree<STATETYPE, TRANSITIONTYPE>.TreeNode> ();
			treeFrontiers.Add (testTree.Root);

			if (computeStateCover)
				stateCoverSet = new List<Word> ();

			transitionCoverSet = new List<Word> ();
			//* epsilon always belong to it!
			transitionCoverSet.Add (new Word ());
			//* and also to this one!
			if (computeStateCover)
				stateCoverSet.Add (new Word ());

			//* at the same time of generating tree, generate the coverage set
			List<Word> coverSetFrontier = new List<Word> ();
			coverSetFrontier.Add (new Word ());

			List<short> nodeLevelInTree = new List<short> ();

			for (int i = 0; i < testModel.Size; i++)
				nodeLevelInTree.Add (short.MaxValue);

			//nodeLevelInTree[0] = 0;
			int currentLevel = -1;

			while (treeFrontiers.Count > 0) {
				int numberOfFrontiers = treeFrontiers.Count;
				currentLevel++;

				for (int i = 0; i < numberOfFrontiers; i++) {

					STATETYPE currenrState = treeFrontiers [0].NodeObject;
					Tree<STATETYPE, TRANSITIONTYPE>.TreeNode currentNodeInTree = treeFrontiers [0];
					treeFrontiers.RemoveAt (0);
					Word currentWord = coverSetFrontier [0];
					coverSetFrontier.RemoveAt (0);

					if (!transitionCoverSet.Contains (currentWord))
						transitionCoverSet.Add (currentWord);

					if (nodeLevelInTree [testModel.IndexOf (currenrState)] < currentLevel) {
						//* This node should be considered as a leaf: dot't expand it.
						continue;
					}


					//* Else: Add this to frontiers
					nodeLevelInTree [testModel.IndexOf (currenrState)] = (short)currentLevel;
					int iii = 0;
					foreach (TRANSITIONTYPE t in testModel.TransitionsOf(currenrState)) {
						Word myWord;
						//myWord = currentWord.Clone();
						if (iii == 0)
							myWord = currentWord;
						else
							myWord = currentWord.Clone ();
						iii++;

						if (t is MealyMachine.Mealy_Transition) {
							myWord.AddSymbol ((t as MealyMachine.Mealy_Transition).inLabel);

							if (computeStateCover) { //ma sto pezzo non dovrebbe essere anche in DFA??
								//* the state cover will be added only if the state was not reached before
								if (nodeLevelInTree [testModel.IndexOf (testModel.DestinationOf (t))] < currentLevel &&
								    !stateCoverSet.Contains (myWord)) {
									Word myWord2 = myWord.Clone ();
									stateCoverSet.Add (myWord2);
								}
							}
						} else if (t is DFA.DFA_Transition) {
							myWord.AddSymbol ((t as DFA.DFA_Transition).Label);
						} else {
							throw new Exception ("W-Method is working only with DFAs and Mealy machines!");
						}

						Tree<STATETYPE, TRANSITIONTYPE>.TreeNode tempNode = currentNodeInTree.AddChild (testModel.DestinationOf (t), t);
						treeFrontiers.Add (tempNode);
						coverSetFrontier.Add (myWord);
					}
				}
			}

			//Console.Write("Transition cover set:");
			//ListUtil.WriteList(transitionCoverSet);
			//Console.Write("\nState cover set:");
			//ListUtil.WriteList(stateCoverSet);
		}
		#endregion
		/// <summary>
		/// Process P and W to become ready to generate test sequences/test suite
		/// </summary>
		public virtual void Process ()
		{
			if (processed)
				return;
			processed = true;
			//Console.WriteLine("1!");
			ComputeCharachterizationSet ();
			//Console.WriteLine("2!");
			FindTransitionCoverSet ();
			//Console.WriteLine("3!");
		}

		/// <summary>
		/// Create a new two dimentional array ([size][size])
		/// </summary>
		/// <typeparam name="T">of type T</typeparam>
		/// <param name="arr"></param>
		/// <param name="size">size of array</param>
		/// <returns></returns>
		T[][] NewTwoDimArray<T> (int size, int size2)
		{
			T[][] arr;
			arr = new T[size][];
			for (int i = 0; i < size; i++)
				arr [i] = new T[size2];
			return arr;
		}

		/// <summary>
		/// it is used in ComputeDistingiushingWords
		/// </summary>
		/// <param name="stateTransitionTable"></param>
		/// <param name="partition">representation of partition</param>
		/// <param name="numberOfTransitions">number of transitions (size of input alphabet)</param>
		/// <param name="indexOfS1">index of first state</param>
		/// <param name="indexOfS2">index of second state</param>
		/// <returns>the different column, -1 if the same</returns>
		int SameRow (int[][] stateTransitionOutputTable, int[][] stateTransitionTable, int[] partition, int numberOfTransitions, int indexOfS1, int indexOfS2)
		{
			/*Console.WriteLine ("{"+indexOfS1 + "-" + indexOfS2);
			for (int y=0; y<partition.Length; y++)
				Console.Write (partition [y] + " ");
			Console.WriteLine ("}");
			*/
			for (int i = 0; i < numberOfTransitions; i++) {
				//* if the destination does't exist
				if (stateTransitionTable [indexOfS1] [i] == -1 && stateTransitionTable [indexOfS2] [i] == -1)
					continue;

				if (stateTransitionTable [indexOfS1] [i] == -1 || stateTransitionTable [indexOfS2] [i] == -1)
					return i;

				//* if they result to the same output and to states in the same partition!
				if (partition [stateTransitionTable [indexOfS1] [i]] == partition [stateTransitionTable [indexOfS2] [i]]
				    && 
				    stateTransitionOutputTable [indexOfS1] [i] == stateTransitionOutputTable [indexOfS2] [i])
					continue;
				return i;
			}
			return -1;
		}

		/// <summary>
		/// Clone an array of integers
		/// </summary>
		/// <param name="arr"></param>
		/// <returns></returns>
		int[] CloneArray (int[] arr)
		{
			int[] c = new int[arr.Length];
			for (int i = 0; i < c.Length; i++)
				c [i] = arr [i];
			return c;
		}

		/// <summary>
		/// Computing the set of distinguihinhg words by construcing the k-equivalence partitions of M
		/// <para>
		/// Characterization set for machine M, denoted as W, is a finite
		/// set of input sequences that distinguish the behavior of any
		/// pair of states in M.
		/// </para>
		/// </summary>
		/// <param name="computeAll">also store distinguishing words for each pair of </param>
		protected List<Word> ComputeCharachterizationSet (bool computeAll = false)
		{
			//* if the set was given as the construction parameters (for example,
			//* when using automata learning, we have this set), don't compute it again
			if (DistinguishingWords != null && !computeAll)
				return null;

			DistinguishingWords = new List<Word> ();
			List<Word> DistinguishingWords4Pairs = null;
			if (computeAll)
				DistinguishingWords4Pairs = new List<Word> ();

			int[] partitionTable = new int[this.testModel.Size];

			Alphabet inputAlphabet = null;
			if (testModel is MealyMachine) {
				inputAlphabet = (testModel as MealyMachine).InputAlphabet;
			} else if (testModel is DFA) {
				inputAlphabet = (testModel as DFA).InputAlphabet; //automa a stati finiti
			} else
				throw new Exception ("W-Method is working only with DFAs and Mealy machines!");

			List<int> groupHeaders = new List<int> ();
			List<List<int>> groups = new List<List<int>> ();

			//* state 0 is in group 0
			groupHeaders.Add (0);              
			groups.Add (new List<int> ());
			groups [0].Add (0);

			#region Compute k-equivalence partitions
			#region Initialize

			//* initialize groups [compute 1-equivalence partition]  
			//* for each state do:
			for (int stateNumber = 1; stateNumber < testModel.Size; stateNumber++) {
				bool groupFound = false;
				//* compare state's output with other goups
				for (int j = 0; j < groupHeaders.Count; j++) {
					bool itIsOk = true;
					foreach (ISymbol symb in inputAlphabet.AllSymbols()) {
						ISymbol o1 = null, o2 = null;

						//* check in state stateNumber
						foreach (TRANSITIONTYPE t in testModel.TransitionsOf(testModel[stateNumber])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o1 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;

							}
						}

						//* check in the header
						foreach (TRANSITIONTYPE t in testModel.TransitionsOf(testModel[groupHeaders[j]])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o2 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;
							}
						}

						if (!((o1 == null && o2 == null) || (o1 != null && o1.Equals (o2)))) {
							itIsOk = false;
							break;
						}
					}
					if (itIsOk) {
						partitionTable [stateNumber] = j;
						groups [j].Add (stateNumber);
						groupFound = true;
						break;
					}
				}
				if (!groupFound) {
					//* it is the header of a new group
					groupHeaders.Add (stateNumber);

					partitionTable [stateNumber] = groupHeaders.Count - 1;

					groups.Add (new List<int> ());
					groups [groups.Count - 1].Add (stateNumber);
				}
			}

			//* convert the state space to matrix: we will need it!
			//FIXME: this is state transition target table
			int[][] stateTransitionTable = NewTwoDimArray<int> (testModel.Size, inputAlphabet.Size);

			int[][] stateTransitionOutputTable = NewTwoDimArray<int> (testModel.Size, inputAlphabet.Size);

			Alphabet outputAlpha = new Alphabet ();

			//* for each state
			for (int i = 0; i < testModel.Size; i++) {
				//* for each symbol in the alphabet
				for (int j = 0; j < inputAlphabet.Size; j++) {
					MealyMachine.Mealy_State target = null;
					ISymbol ot = null;

					//find the target state for symb[j]
					//FIXME: we can simply use IndexOf!
					//* for each transition
					for (int k = 0; k < testModel.TransitionsOf(testModel[i]).Count; k++) {
						if ((testModel.TransitionsOf (testModel [i]) [k] as MealyMachine.Mealy_Transition).inLabel.
						    Equals (inputAlphabet.AllSymbols () [j])) {
							target = (testModel.TransitionsOf (testModel [i]) [k] as MealyMachine.Mealy_Transition).Destination;
							ot = (testModel.TransitionsOf (testModel [i]) [k] as MealyMachine.Mealy_Transition).outLabel;
							break;
						}
					}
					int targetIndex = -1;
					int outputIndex = -1;

					//* find index of target in the machine
					if (target != null) {
						for (int l = 0; l < testModel.Size; l++) {
							if (target == (testModel [l] as MealyMachine.Mealy_State)) {
								targetIndex = l;
								if (outputAlpha.Rank (ot) != -1) {
									outputIndex = outputAlpha.Rank (ot);
								} else {
									outputAlpha.AddSymbol (ot);
									outputIndex = outputAlpha.Rank (ot);
								}
								break;
							}
						}
					}

					//* set the value in table
					stateTransitionTable [i] [j] = targetIndex;
					stateTransitionOutputTable [i] [j] = outputIndex;
				}
			}

			#endregion

			List<int[]> listOfPartitionTables = new List<int[]> ();
			listOfPartitionTables.Add (CloneArray (partitionTable));

			List<int> toBeSeparated = new List<int> ();
			int numberOfGroups = groups.Count;

			//* continue till converging the algorithm
			while (true) {
				bool somethingChanged = false;

				int[] tempPartion = CloneArray (partitionTable);

				//* create groups from scratch
				groups.Clear ();
				for (int i=0; i<numberOfGroups; i++)
					groups.Add (new List<int> ());
				for (int i=0; i<partitionTable.Length; i++)
					groups [partitionTable [i]].Add (i);


				for (int currentGroup = 0; currentGroup < groups.Count; currentGroup++) {
					//* this group has only one state
					if (groups [currentGroup].Count == 1)
						continue;

					//* index1 in the group
					for (int i = 1; i < groups[currentGroup].Count; i++) {
						//* index2 in the group

						int state1, state2, state3;

						state1 = groups [currentGroup] [0];
						state2 = groups [currentGroup] [i];

						//* check the groups of destinations for the two row
						int eq = SameRow (stateTransitionOutputTable, stateTransitionTable, partitionTable, inputAlphabet.Size, state1, state2);
						if (eq != -1) {
							somethingChanged = true;
							//* add a new group!
							numberOfGroups++;
							toBeSeparated.Clear ();
							toBeSeparated.Add (i);

							//* find all of those that have equal row with state2
							for (int j = i + 1; j < groups[currentGroup].Count; j++) {
								state3 = groups [currentGroup] [j];

								//* check other elements in the group: they are similar to index1 or not?
								int eq2 = SameRow (stateTransitionOutputTable, stateTransitionTable, partitionTable, inputAlphabet.Size, state2, state3);
								if (eq2 == -1) {
									toBeSeparated.Add (j);
									//[Ali]: I comment this (17 March 2015)
									//groups [currentGroup].RemoveAt (j);
								}
							}

							//* and add all different state into that group
							for (int y = 0; y<toBeSeparated.Count; y++) {
								int indexOfDiffState = toBeSeparated [y];
								int diffState = groups [currentGroup] [indexOfDiffState];
								tempPartion [diffState] = numberOfGroups - 1;
							}
							//* remove 'separateds' from current group
							for (int y = 1; y<toBeSeparated.Count; y++) {
								groups [currentGroup].RemoveAt (y);
							}
						}
					}
				}

				//* this will happen when it converged
				if (!somethingChanged)
					break;
				else {
					//* store partition table
					listOfPartitionTables.Add (CloneArray (tempPartion));
					partitionTable = tempPartion;
				}
			}

			#endregion

			//Console.WriteLine("The system is "+listOfPartitionTables.Count+"-distinguishable!");                        

			if (groups.Count != testModel.Size)
				throw new Exception ("The model is not minimal!");


			//* now, from list of partitions:
			//* find the distinguishing string for each pair of states
			for (int i = 0; i < testModel.Size; i++) {
				for (int j = i + 1; j < testModel.Size; j++) {
					int state1 = i, state2 = j;

					//int startFrom = listOfPartitionTables.Count - 1;
					int startFrom = 0;

					//* find the partition that state i and state j are different
					for (int k = 0; k <listOfPartitionTables.Count; k++) {
						//for (int k = listOfPartitionTables.Count - 2; k >= 0; k--) {
						if (listOfPartitionTables [k] [state1] != listOfPartitionTables [k] [state2])
							//if (listOfPartitionTables [k] [state1] == listOfPartitionTables [k] [state2])//vuol dire che gli stati sono nello stesso gruppo
							break;
						startFrom ++;                    
					}


					Word w = new Word ();

					//* from that partition, go backward
					for (int k = startFrom; k >= 0; k--) {
						int l = SameRow (stateTransitionOutputTable,stateTransitionTable,listOfPartitionTables [k], inputAlphabet.Size, state1, state2);

						/*
						Console.WriteLine (state1 + "-" + state2);
						Console.WriteLine ("K="+k);
						Console.WriteLine ("L="+l);
						for (int y=0; y<listOfPartitionTables[k].Length; y++)
							Console.Write (listOfPartitionTables [k] [y] + " ");
						Console.WriteLine ();

						if (l == -1) {
							Console.WriteLine("Error in W-Method! Ignore and continue...");
							break;
						}*/

						w.AddSymbol (inputAlphabet.AllSymbols () [l]);
						//Console.Write(inputAlphabet.AllSymbols()[l]+" . ");
						state1 = stateTransitionTable [state1] [l];
						state2 = stateTransitionTable [state2] [l];

					}

					foreach (ISymbol symb in inputAlphabet.AllSymbols()) {
						ISymbol o1 = null, o2 = null;

						if (state1 == -1 || state2 == -1)
							break;

						//* check in state stateNumber
						foreach (TRANSITIONTYPE t in testModel.TransitionsOf(testModel[state1])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o1 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;
							}
						}

						//* check in the header
						foreach (TRANSITIONTYPE t in testModel.TransitionsOf(testModel[state2])) {
							if ((t as MealyMachine.Mealy_Transition).inLabel.Equals (symb)) {
								o2 = (t as MealyMachine.Mealy_Transition).outLabel;
								break;
							}
						}

						if (!((o1 == null && o2 == null) || (o1 != null && o1.Equals (o2)))) {
							//Console.Write(symb+" * ");
							w.AddSymbol (symb);
							break;
						}
					}

					//Console.WriteLine("Add-");
					if (computeAll)
						DistinguishingWords4Pairs.Add (w);

					if (!DistinguishingWords.Contains (w))
						DistinguishingWords.Add (w);
				}
			}

			//ListUtil.WriteList(DistinguishingWords, "\n**");
			//Console.ReadKey();
			return DistinguishingWords4Pairs;
		}

		/// <summary>
		/// Instead of Generating the whole test sequences, we better generate them one by one!
		/// </summary>
		/// <returns>enumarated test cases</returns>
		public virtual IEnumerable TestSequences ()
		{
			if (!processed)
				throw new Exception ("You should first use 'Process()'!");

			for (int i = 0; i < this.transitionCoverSet.Count; i++) {
				for (int j = 0; j < this.DistinguishingWords.Count; j++) {
					Word testCase = transitionCoverSet [i].Clone ();
					testCase.AddWord (DistinguishingWords [j]);
					yield return testCase;
				}
			}
		}

		/// <summary>
		/// We can also generate the whole test suite (which is more memory/time consuming)
		/// </summary>
		/// <returns>the generated test suite</returns>
		public List<Word> GenerateTestSuite ()
		{
			if (!processed)
				throw new Exception ("You should first use 'Process()'!");

			List<Word> testSuite = new List<Word> ();
			foreach (Word testCase in TestSequences()) {                
				//* check that if the subset exist, removed it!
				for (int i=0; i<testSuite.Count; i++) {
					if (testSuite [i].IsPrefixOf (testCase))
						testSuite.RemoveAt (i);
				}
				testSuite.Add (testCase);
			}
			return testSuite;
		}
	}
}
